\documentclass[a4paper]{article}
\usepackage[a4paper,margin=2cm,top=2.0cm,bottom=2.34cm]{geometry}
\usepackage[spanish,activeacute]{babel}
\usepackage[T1]{fontenc}
\usepackage{algo2symb}
\usepackage{newalgo}
\usepackage{tad}
\usepackage{itef}

\parskip=1.5ex
\pagestyle{empty}

\begin{document}
\begin{center}\textbf{\Large M'odulo \nombretad{multiconj\_stock}}\\
Se explica con la especificaci'on de multiconj\_stock
\end{center}

\medskip
\medskip
\medskip

\begin{tad}{multiconj\_stock}

	\usa{multiconj\_extendido(material)}
	\exporta{}
	
	\generadores
		\func{$\emptyset$}{nat/tam}{multiconj\_stock}{}
		\func{Ag}{material/m, multiconj\textunderscore stock/ms}{multiconj\_stock}{m<tam(ms)}
		
	\observadores
		\func{tam}{multiconj\textunderscore stock}{nat}{}
		\func{VerMulticonj}{multiconj\textunderscore stock}{multiconj\_extendido(material)}{}

	\otrasops
		\func{AgMuchos}{material/m, nat, multiconj\textunderscore stock/ms}{multiconj\_stock}{m<tam(ms)}
		\func{Array2multiconj}{arreglo\textunderscore dimensionable}{multiconj\_stock}{}
		
	\axiomas
		\axioma{tam($\emptyset$(tam))}{tam}
		\axioma{tam(Ag(m,ms))}{tam(ms)}
		\\
		\axioma{VerMulticonj($\emptyset$(tam))}{$\emptyset$}
		\axioma{VerMulticonj(Ag(m,ms))}{Ag(m,VerMulticonj(ms))}
		\\
		\axioma{AgMuchos(m,n,ms)}{$\LIF$ n=0 $\LTHEN$ ms $\LELSE$ AgMuchos(m,n-1,Ag(m,ms)) $\LFI$}
		\\
		\axioma{Array2multiconj(crearArreglo(n))}{$\emptyset$(n)}
		\axioma{Array2multiconj(a[m] $\leftarrow$ c)}{AgMuchos(m,c,Array2multiconj(a))}
\end{tad}

\medskip
\medskip
\medskip

\noindent \textbf{Representaci'on}
\\
\texttt{multiconj\_stock} se representa con \texttt{estr\_multiconj\_stock}\\
donde \texttt{estr\_multiconj\_stock} es\\ \hspace*{1em}<cantidad: \texttt{arreglo\_dimensionable}(<cant:\texttt{nat} $\times$ enHeap:\texttt{nat}>) $\times$ heap: \texttt{arreglo\_dimensionable(nat)}>

\medskip
\medskip
\medskip

\noindent \textbf{generos:} \texttt{multiiconj\_stock}

\medskip
\medskip
\medskip

\noindent \textbf{Invariante de Representaci'on}
\\
\texttt{El array  y el heap tienen el mismo tama'no.}\\
\texttt{Todas las posiciones de los dos arreglos estan definida.}\\
\texttt{Para todo elemento del arreglo cantidad su componente \textsc{enHeap} representa la posici'on\\ en el Heap  y para todo elemento del Heap su valor representa el 'indice en el arreglo cantidad.}\\
\texttt{Para todo elemento \textsc{n}  en el heap sus hijos (2i+1 y 2i+2),si existen, tienen menor cantidad que el elemento \textsc{n}.}
\\
$Rep\!:$ \texttt{estr\_multiconj\_stock} $\rightarrow$ \texttt{bool}\\
\hspace*{1em}($\forall$ $e\!:$ \texttt{estr\_multiconj\_stock}) $Rep(e)$ $\equiv$ \\
\hspace*{2em}$tam(e.cantidad)=tam(e.heap)$ $\yluego$ \\
\hspace*{2em}($\forall$ $i\!:$ \texttt{nat})($i < tam(e.heap)$) $\impluego$ \\
\hspace*{3em}$def?(i,e.heap) \wedge def?(i,e.cantidad)$ \\
\hspace*{3em}$\yluego$ $e.heap[e.cantidad[i].enHeap]=i$ \\
\hspace*{3em}$\wedge$ $(2*i+1 < tam(e.heap)) \impluego e.cantidad[e.heap[2*i+1]].cant < e.cantidad[e.heap[i]].cant$ \\
\hspace*{3em}$\wedge$ $(2*i+2 < tam(e.heap)) \impluego e.cantidad[e.heap[2*i+2]].cant < e.cantidad[e.heap[i]].cant$ \\
\hspace*{2em})

\medskip
\medskip

\noindent \textbf{Funci'on de Abstracci'on}
\\
\texttt{Para todos los elementos, \#(i en el multiconjunto) es la componente \textsc{cant} de ese elemento.}
\\
$Abs\!:$ \texttt{estr\_multiconj\_stock} $\rightarrow$ \texttt{multiconj\_stock} \hspace*{3em} (Rep(e))\\
\hspace*{1em} $Abs(e)$ $\equiv$ $ms \diagup .$\\
\hspace*{2em} ($\forall$ $i\!:$ \texttt{nat})($i < tam(e.cantidad) \impluego \#(i,VerMulticonj(ms))=e.cantidad[i].cant$) \\

\medskip

\noindent \textbf{Interfaz}

\comentario{\Ode{cantidad}}
\begin{algorithm}{Vacio}{\param{in}{cantidad}{nat}}{res\!: multiconj\_stock}
\{\true\}\\
\{res \igobs \emptyset(cantidad)\}
\end{algorithm}

\comentario{\Ode{tam(ms)}}
\begin{algorithm}{Vacio}{\param{in}{ms}{multiconj\_stock}}{res\!: bool}
\{\true\}\\
\{res=\emptyset?(VerMulticonj(ms))\}
\end{algorithm}

\begin{algorithm}{cantMateriales}{\param{in}{ms}{multiconj\_stock}}{res\!: nat}
\{\true\}\\
\{res=tam(ms)\}
\end{algorithm}

\comentario{\Ode{log(tam(ms))}}
\begin{algorithm}{Agregar}{\param{in}{m}{material},\param{in}{c}{nat},\param{inout}{ms}{multiconj\_stock}}{}
\{ms \igobs ms_0\ \wedge m<tam(ms)\}\\
\{ms \igobs AgMuchos(m,c,ms_0) \}
\end{algorithm}

\comentario{\Ode{1}}
\begin{algorithm}{Cardinal}{\param{in}{m}{material},\param{in}{ms}{multiconj\_stock}}{res\!: nat}
\{\true\}\\
\{res \igobs \#(m,VerMulticonj(ms))\}
\end{algorithm}

\comentario{\Ode{log(tam(ms))}}
\begin{algorithm}{Sacar}{\param{in}{m}{material},\param{in}{c}{nat},\param{inout}{ms}{multiconj\_stock}}{}
\{ms \igobs ms_0\}\\
\{VerMulticonj(ms) \igobs VerMulticonj(ms_0) \setminus Rep(m,c)\}
\end{algorithm}

\comentario{\Ode{1}}
\begin{algorithm}{ElQueMasHay}{\param{in}{ms}{multiconj\_stock}}{res\!: material}
\{\neg \emptyset?(VerMulticonj(ms))\}\\
\{res \igobs DameUno(MasAparecen(VerMulticonj(ms)))\}
\end{algorithm}

\comentario{\Ode{tam(arr)}}
\begin{algorithm}{ActualizarStock}{\param{in}{arr}{arreglo\_dimensionable(nat)}, \param{inout}{ms}{multiconj\_stock}}{}
\{tam(arr) \igobs tam(ms)\}\\
\{ms \igobs Array2multiconj(arr)\}
\end{algorithm}

\noindent \textbf{Algoritmos}
\medskip

\begin{algorithm}{iVacio}{\param{in}{cantidad}{nat}}{res\!: estr\_multiconj\_stock}
res.cantidad \= crearArreglo(cant)\\
res.heap \= crearArreglo(cant)\\
\begin{FOR}{i \= 0 \TO cant}
	res.cantidad[i] \= <0,i>\\
	res.heap[i] \= i\\
\end{FOR}\\
\comentario{lineas 1-5 son \Ode{1}, y lineas 3-5 se repiten \texttt{cantidad} veces.}\\
\comentario{Complejidad: \Ode{\texttt{cantidad}}}
\end{algorithm}


\begin{algorithm}{iVacio}{\param{in}{ms}{estr\_multiconj\_stock}}{res\!: bool}
i:nat \= 0\\
res \= true\\
\begin{WHILE}{i < tam(ms.cantidad) \land res}
\begin{IF}{ms.cantidad[i].cant > 0}
		res \= false\\
\end{IF}\\
i \= i + 1\\
\end{WHILE}\\
\comentario{lineas 1-7 son \Ode{1}, y lineas 2-5 se repiten a lo sumo \texttt{tam(ms.cantidad)} veces.}\\
\comentario{Complejidad: \Ode{\texttt{tam(ms)}}}
\end{algorithm}

\begin{algorithm}{iCantMateriales}{\param{in}{ms}{estr\_multiconj\_stock}}{res\!: nat}
res \= tam(ms.cantidad)\\
\comentario{Complejidad: \Ode{\texttt{1}}}
\end{algorithm}


\begin{algorithm}{iAgregar}{\param{in}{m}{material},\param{in}{c}{nat},\param{inout}{ms}{estr\_multiconj\_stock}}{}
ms.cantidad[m].cant \= ms.cantidad[m].cant + c\\
subir(ms.cantidad[m].enHeap,ms.heap,ms.cantidad)\\\\
\comentario{linea 1 es \Ode{1}, y linea 2 es \Ode{log(ms.cantidad[m].enHeap)}  (ver abajo)}\\
\comentario{Complejidad: \Ode{log(tam(ms))}}
\end{algorithm}


\begin{algorithm}{aux subir}{\param{in}{posini}{nat}, \param{inout}{arr}{arreglo\_dim(nat)}, \param{inout}{prioridades}{arreglo\_dim(<nat \times nat>)}}{pos\!: nat}	
pos:nat \= posini\\
\begin{WHILE}{\neg(pos \equiv 0) \wedge prioridades[arr[floor((pos-1)/2)]].cant < prioridades[arr[pos]].cant)}
swap(pos,floor((pos-1)/2),arr,prioridades)\\
pos \= floor((pos-1)/2)\\
\end{WHILE}\\
\comentario{lineas 1-4 son \Ode{1} , y lineas 2-4 se repiten a lo sumo log(posini) veces. (siempre lo divide a la mitad hasta que quede 1)}\\
\comentario{Complejidad: \Ode{log(posini)}}
\end{algorithm}

\begin{algorithm}{aux swap}{\param{in}{m}{nat}, \param{in}{n}{nat}, \param{inout}{arr}{arreglo\_dim(nat)}, \param{inout}{prioridades}{arreglo\_dim(<nat \times nat>)}}{}
	tmp:nat \= arr[m]\\
	arr[m] \= arr[n]\\
	arr[n] \= tmp\\
	prioridades[arr[m]].enHeap \= n\\
	prioridades[arr[n]].enHeap \= m\\
\comentario{lineas 1-5 son \Ode{1}}\\
\comentario{Complejidad: \Ode{1}}
\end{algorithm}


\begin{algorithm}{iCardinal}{\param{in}{m}{material},\param{in}{ms}{estr\_multiconj\_stock}}{res\!: nat}
	res \= ms.cantidad[m].cant\\\\
\comentario{Complejidad: \Ode{1}}
\end{algorithm}
\\

\begin{algorithm}{iSacar}{\param{in}{m}{material},\param{in}{c}{nat},\param{inout}{ms}{estr\_multiconj\_stock}}{}
	ms.cantidad[m].cant \= ms.cantidad[m].cant - c\\
	bajar(ms.cantidad[m].enHeap,ms.heap,ms.cantidad)\\\\
\comentario{linea 1 es \Ode{1}, y bajar es \Ode{log(\frac{tam(ms)}{2*ms.cantidad[m].enHeap})} (ver abajo)}\\
\comentario{que en el peor caso es Complejidad: \Ode{log(tam(ms))}}
\end{algorithm}

\begin{algorithm}{aux bajar}{\param{in}{posini}{nat}, \param{inout}{arr}{arreglo\_dim(nat)}, \param{inout}{prioridades}{arreglo\_dim(<nat \times nat>)}}{pos\!: nat}
	pos:nat \= posini\\
	\begin{WHILE}{(2*pos+1<tam(arr) \wedge prioridades[arr[2*pos+1]].cant > prioridades[arr[pos]].cant)\\ 
		\hspace*{3em}\vee (2*pos+2 < tam(arr) \wedge prioridades[arr[2*pos+2]].cant > prioridades[arr[pos]].cant)}
		\begin{IF}{2*pos+2 < tam(arr) \wedge prioridades[arr[2*pos+2]].cant > prioridades[arr[2*pos+1]].cant}
			swap(pos,2*pos+2,arr,prioridades)\\
			pos \= 2*pos+2
		\ELSE
			swap(pos,2*pos+1,arr,prioridades)\\
			pos \= 2*pos+1\\
		\end{IF}
	\end{WHILE}\\
	\comentario{Todas las Operaciones son \Ode{1}, y el ciclo se ejecuta hasta que \texttt{pos} $\geq$ tam(arr)/2, duplicandose en cada paso.}\\
	\comentario{Osea, que $\frac{tam(arr)/2}{posini}$ es la relacion entre las variables}\\
	\comentario{y el ciclo se ejecuta $log_2(\frac{tam(arr)}{2 posini})$ veces.}\\
	\comentario{Complejidad: \Ode{log(\frac{tam(arr)}{2 posini})}}
\end{algorithm}


\begin{algorithm}{iElQueMasHay}{\param{in}{ms}{estr\_multiconj\_stock}}{res\!: material}
	res \= ms.heap[0]\\
\comentario{Complejidad: \Ode{1}}
\end{algorithm}


\begin{algorithm}{iActualizarStock}{\param{in}{arr}{arreglo\_dimensionable(nat)}, \param{inout}{ms}{estr\_multiconj\_stock}}{}
	\begin{FOR}{i \= 0 \TO tam(ms.cantidad)}
		ms.cantidad[i].cant \= arr[i]\\
	\end{FOR}\\
	pos \= floor((tam(ms.heap)-1)/2)\\
	\begin{WHILE}{pos>0}
		bajar(pos,ms.heap,ms.cantidad)\\
		pos \= pos-1
	\end{WHILE}
\end{algorithm}\\
	\comentario{Llamamos n a tam(a).}\\
	\comentario{Este algoritmo recorre el arreglo y luego aplica n/2 veces \textsc{bajar} con los valores de \texttt{pos} desde n/2 hasta 0}\\
	\comentario{Complejidad del algoritmo: $$n+\sum_{pos=1}^{n/2}log_2(\frac{n}{2pos}) = n+log_2(\prod_{pos=1}^{n/2}\frac{n/2}{pos})$$}
	\comentario{Que tiene la misma complejidad que $$n+log(\prod_{pos=1}^{n}\frac{n}{pos}) = n+log(\frac{n^n}{n!})$$}
	\comentario{Esto es \Ode{n} porque $$\mathop{\lim}\limits_{n\to\infty}\frac{n+log(\frac{n^n}{n!})}{n} = \mathop{\lim}\limits_{n\to\infty}\frac{n}{n}+\frac{log(\frac{n^n}{n!})}{n} = \mathop{\lim}\limits_{n\to\infty}\frac{log(\frac{n^n}{n!})}{n} = 1$$}
	\comentario{$\Rightarrow$ Complejidad: \Ode{\texttt{tam(a)}}}

\end{document}
